COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	contro[w85,jmc]		How to control reasoning
C00011 00003
C00013 00004	Areas to try
C00014 00005	map coloring
C00015 00006	Mental state and physical state
C00020 00007	dbb(goal(at(x,l),s),ss)
C00021 ENDMK
C⊗;
contro[w85,jmc]		How to control reasoning

	Since the early 1970s and maybe earlier, perhaps even in my
own work, it has been proposed that the right way to control
a theorem prover is to give it sentences about what it ought to
do.  However, no-one has succeeded in determining the form
of these sentences or how a theorem prover should use them.
Here is a tentative proposal for solving the problem.

	We use an object language and a metalanguage.  All deduction
is done in the metalanguage.
It would be nice if the metalanguage were
what logicians have called
{\it monogenic}, i.e. only one deduction is possible in any state
of the prover.  However, if the metalanguage is first order,
this isn't possible, since conjunctions of known facts can always
be deduced.  We may be able to arrange it that the metalanguage language
will recommend only one object language deduction in a given state.
This will be made more precise later.

	The object language has its rules of inference,
and corresponding to each rule in the object language is a sentence
of the metalanguage.  This sentence says that the inference is
possible provided its object language premisses are in the
database and provided certain other  conditions are met.  These other
conditions are designed to carry the heuristics that say that the
deduction is not only legitimate but appropriate to be made at
the given time.

	This may not be right.  What we really want is that among
all the deductions permissible in the object language taken per
se, in a given state of an object language database, the metalanguage
allows only one deduction.  The simplest case would be a propositional
object language.

	For example, suppose one object language rule is modus ponens.
Let $p$ and $q$ be variables ranging over wffs of the object language
and let $p imp q$ be our object notation for material implication.
The corresponding metalanguage sentence is
%
$$∀p q ss.db(p,ss) ∧ db(p imp q,ss) ∧ do(modus(p,q),ss) ⊃ db(q,next ss).$$
%
	Here $ss$ denotes a state of the reasoning process.  $db(p,ss)$
is the assertion that $p$ is in the database in the state $ss$.
$next ss$ is the next state of the reasoning process after $ss$.  The
wff $do(modus(p,q),ss)$ may contain any conditions we like about whether
it is appropriate to do this modus ponens.  Ideally there should be
exactly one appropriate inference to make.  Notice that the step
will be correct in the object language just provided the object
language admits modus ponens as a correct rule of inference.

	Other object-langage rules of inference are to be
represented by corresponding metalanguage sentences, and
a succession of mental states is defined, each $next$ of
the preceding.

	All the heuristic information is contained in the
predicate $do$.  It may refer to what kinds of sentences
are present in the database $ss$.  It will be a conjunction
containing a condition that will prevent deducing
something that is already in the database.

Alternatives:

	Maybe $next ss$ would be appropriate only if the
system were genuinely monogenic.  Therefore, we may want to
relax (zz1) to read

$$∀p q ss ss1.db(p,ss) ∧ db(p imp q,ss) ∧ ok(modus(p,q),ss) ∧
(∀r.db(r,ss1) ≡ r = q ∨ db(r,ss)) ⊃ maysucceed(ss,ss1).$$

We then imagine that the system computes successive mental
states $(ss1,ss2,\ldots)$ where each succeeding pair satisfies
$maysucceed$.

Example:

	Let's see if we can do it for the STRIPS blocks world
as described in (McCarthy 1985).

	The language of of that paper is first order logic with
reified propositions.  Therefore, in order to apply our method
it looks like we need a metametalanguage with respect to the
reified propositions.  We need a physical database denoted by
$s$ and our mental database denoted by $ss$.  We'll use
$db(on(x,y),s)$ for the proposition that $x$ is on $y$ in the
physical database $s$, and therefore we need a wff.
$dbb(p,ss)$ asserting that a sentence $p$ is in the mental database
$ss$.  An example will be $dbb(db(on(x,y),s),ss)$.

	While we took the logic of that paper as full first order
logic, we didn't use all the power of first order logic.
Therefore, we'll try to get by with a subset, perhaps with only
free variables implicitly quantified and constants.

	Consider first the STRIPS axiom written
%
$$\eqalign{%
&∀p a s.db(p,result(a,s))\cr
& ≡ if ¬precondition(a,s) then db(p,s)
else db(p,s) ∧ ¬deleted(p,a,s) ∨ add(p,a,s)}$$
%
in that paper.

	Since we want it to always be true, perhaps we can write
%
$$\eqalign{%
&∀ss p a s.dbb(db(p,result(a,s))\cr
& equiv if not precondition(a,s) then db(p,s)
else db(p,s) and not deleted(p,a,s) or add(p,a,s),ss)}$$
%
If it turns out to be more convenient we could also prescribe it
for an initial mental state $ss0$ and provide for its being preserved.
Next in that paper we had the assertion that the blocks are all different
%
$$a≠b∧a≠c∧a≠d∧a≠Table∧b≠c∧b≠d∧b≠Table∧c≠d∧c≠Table∧d≠Table.$$
%
which we will try to leave as is.  However, we shall need to
provide for importing constants into the o
*****

try rewriting the STRIPS axiom to include the next mental state and
to put the conditionals in the metalanguage.

	You don't like the term {\it reification}?  Well, here
comes {\it double reification} and even {\it multiple reification}.
We need double reification, because think-time and act-time
progress differently and therefore require different states.

	Take the simple rule

$$∀x y s.holds(on(x,y),result(move(x,y),s))$$

where we have omitted the usual qualifications.
We change it to

$$∀x y s ss.plaus(move(x,y),s,ss) ⊃ 
dbb(holds(on(x,y),result(move(x,y),s)),next ss)$$

goodidea(ss,update(holds(on(x,y),result(move(x,y),s)),ss))

We can axiomatize  goodidea.  The program may determine the
good ideas and choose the best - or at random among the good.

update(wff,ss) merely adds  wff  to the database.  We can consider
systems in which this is the only way  ss  gets changed.

also  badidea
goal(s,on(x,y)); maybe we don't need this if we have the following.

goal(ss,knowhowtoachieve(on(x,y),s))

holds(wants(john,on(x,y)),s)

dbb(goal(knowhowtoachieve(on(x,y),s)),ss)

achieves(plan,on(x,y),s)

goal(find(plan,achieves(plan,on(x,y),s)),ss)

goal(∃plan.explicit plan ∧ know(achieves(plan,on(x,y),s)),ss)

explicit(plan) excludes plans that like "Call Reagan's secret phone number",
when you don't know the number.
Areas to try

Map coloring
block structure design and construction
Tower of Hanoi
Missionaries and Cannibals
Wise men and Mr S and Mr P?
planning as in Operations Research

What about mental actions and a mental  result(e,ss)?
map coloring

Map coloring is a design problem without the corresponding construction
problem.  That would be walking around the map actually coloring the
countries.

country(CA) ∧ country(AZ), etc.

∀z.country(z,Map1) ≡ z = CA ∨ z = AZ ∨ etc.

The states are all different expressed in one of several ways.

∀x y.next(x,y,Map1) ≡ x = CA ∧ y = AZ ∨ etc.

(Is there some neat way of avoiding listing the symmetric cases
and still preserving the ≡ ?)

db(color(CA,red),s(n))

(How to handle backtracking?  How to handle postponement?  Kempe?)
(Use a successors function?)
Mental state and physical state

	Our use of mental state and physical state will usually
have the following properties.

	1. There will usually be a physical state associated with
each mental state.  It might be called  $now$, although formalizing
the properties of $now$ may turn out to be difficult.  In some cases
the $now$ will be trivial, especially if we have a mathematical or
other purely intellectual problem.

	2. The mental state includes what is believed about $now$.
In the formulas so far, we have merely allowed mental states to
refer to physical states without formally distinguishing one as
now.  Anyway the information about a physical state is meta-ized
in the mental state, i.e. $on(x,y,s)$ becomes $holds(on(x,y,s),ss)$
or $db(on(x,y,s),ss)$.  Perhaps this can often be written
$db(on(x,y,now(ss)),ss)$ or $db(on(x,y,now),ss)$.  The the
updating behavior of this last will be a trifle peculiar and
needs study.  There may be various kinds of mental $now$ as well
as a physical $now$.  I guess there are even several kinds of
physical $now$.  Namely, as I plan my trip to Europe, I think
about a physical $now$ in which I am at Stanford.  It remains
stable as I walk about the room.  Another more detailed $now$
varies as I (say) put things in my suitcase.  Different mental
knows exist as I think about a mathematical problem.  What lemmas
I know and conjecture constitute a $now$ that may not change
for days.  The point is that human thinking and speech seems to use all
these kinds of $now$.  McDermott, Allen and Co. would use time
intervals for these $now$s.

	3. However, beliefs about the current and other physical
states are only a part of the content of a mental state.  There
are also goals, and these goals are both physical and mental.
There is also information about how to achieve the goals and
facts relevant to the goals.

	4. Many facts relevant to goals are directly computable.
For example, it is computable which countries have three or
fewer neighbors.  These computable syntactic facts must play a
role in problem solving.

	5. How can we assert that a country with 3 or fewer
neighbors may be colored last.  Clearly in order to say this,
whether the program needs to backtrack must be assertable.

	6. Human thought often involves thinking about the problem
before plunging in and solving it.  True machine intelligence will
require the same.  Examples: bacterial theory of disease.  Mycin
doesn't know the bacterial theory of disease and cannot be told.
However, this attempt at a new kind of logic programming should
avoid problems that require theoretical or general thinking.

	7. The most obvious predicates of mental state are
db(p,ss) and holds(p,ss).  We my also have  value(exp,ss)
and wants(p,ss).  wants(p,ss)  may be the same as or different
from  db(want p,ss).  We could also have  inconsistent(ss).
dbb(goal(at(x,l),s),ss)